Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
tail(cons(X, XS)) → XS

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
tail: {1}


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
tail(cons(X, XS)) → XS

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
tail: {1}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
tail(cons(X, XS)) → XS

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
tail: {1}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {tail, TAIL} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The collapsing dependency pairs are DPc:

TAIL(cons(X, XS)) → XS


The hidden terms of R are:

zeros

Every hiding context is built from:none

Hence, the new unhiding pairs DPu are :

TAIL(cons(X, XS)) → U(XS)
U(zeros) → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zeros)
tail(cons(X, XS)) → XS

The set Q consists of the following terms:

zeros
tail(cons(x0, x1))


The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 2 less nodes.